[Merged by Bors] - chore(Data/Tree/Basic): Rename Tree to BinaryTree by sorrachai · Pull Request #39707 · leanprover-community/mathlib4

sorrachai · 2026-05-22T14:33:12Z

Rename Tree to BinaryTree.

This frees up the name Tree to cover n-ary trees in future.

We only deprecate the defs, and move the theorems without deprecation.

github-actions · 2026-05-22T14:33:26Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-05-22T14:34:32Z

PR summary 9ab2f22441

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Tree.Basic	58	59	+1 (+1.72%)
Mathlib.Data.Tree.Get	63	64	+1 (+1.59%)
Mathlib.Data.Tree.Traversable	101	102	+1 (+0.99%)

Import changes for all files

Files	Import difference
3 files `Mathlib.Data.Tree.Basic` `Mathlib.Data.Tree.Get` `Mathlib.Data.Tree.Traversable`	1

Declarations diff (regex)

+ BinaryTree.{u}
+ Tree
+ Tree.nil.{u}
+ Tree.node.{u}
+ _root_.Tree.get
+ _root_.Tree.getOrElse
+ _root_.Tree.height
+ _root_.Tree.indexOf
+ _root_.Tree.left
+ _root_.Tree.map
+ _root_.Tree.numLeaves
+ _root_.Tree.numNodes
+ _root_.Tree.right
+ _root_.Tree.traverse
+ _root_.Tree.treesOfNumNodesEq
+ _root_.Tree.unitRecOn
+ instance : Inhabited (BinaryTree α)
+ instance : LawfulTraversable BinaryTree
+ instance : Traversable BinaryTree
- Tree.{u}
- instance : Inhabited (Tree α)
- instance : LawfulTraversable Tree
- instance : Traversable Tree

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 9ab2f22).

+65 new declarations
−50 removed declarations

+BinaryTree
+BinaryTree.below
+BinaryTree.brecOn
+BinaryTree.brecOn.eq
+BinaryTree.brecOn.go
+BinaryTree.casesOn
+BinaryTree.coe_treesOfNumNodesEq
+BinaryTree.comp_map
+BinaryTree.comp_traverse
+BinaryTree.ctorElim
+BinaryTree.ctorElimType
+BinaryTree.ctorIdx
+BinaryTree.get
+BinaryTree.getOrElse
+BinaryTree.height
+BinaryTree.height.eq_def
+BinaryTree.height_le_numNodes
+BinaryTree.id_map
+BinaryTree.indexOf
+BinaryTree.instInhabited
+BinaryTree.instLawfulTraversable
+BinaryTree.instTraversable
+BinaryTree.left
+BinaryTree.left_node_right_eq_self
+BinaryTree.map
+BinaryTree.map.eq_def
+BinaryTree.mem_treesOfNumNodesEq
+BinaryTree.mem_treesOfNumNodesEq_numNodes
+BinaryTree.naturality
+BinaryTree.nil
+BinaryTree.nil.elim
+BinaryTree.nil.sizeOf_spec
+BinaryTree.noConfusion
+BinaryTree.noConfusionType
+BinaryTree.node
+BinaryTree.node.elim
+BinaryTree.node.inj
+BinaryTree.node.injEq
+BinaryTree.node.noConfusion
+BinaryTree.node.sizeOf_spec
+BinaryTree.numLeaves
+BinaryTree.numLeaves.eq_def
+BinaryTree.numLeaves_eq_numNodes_succ
+BinaryTree.numLeaves_pos
+BinaryTree.numNodes
+BinaryTree.numNodes.eq_def
+BinaryTree.pairwiseNode
+BinaryTree.rec
+BinaryTree.recOn
+BinaryTree.right
+BinaryTree.traverse
+BinaryTree.traverse.eq_def
+BinaryTree.traverse_eq_map_id
+BinaryTree.traverse_pure
+BinaryTree.treesOfNumNodesEq
+BinaryTree.treesOfNumNodesEq.eq_def
+BinaryTree.treesOfNumNodesEq_card_eq_catalan
+BinaryTree.treesOfNumNodesEq_succ
+BinaryTree.treesOfNumNodesEq_zero
+BinaryTree.unitRecOn
+BinaryTree.«term_△_»
-Tree.below
-Tree.brecOn
-Tree.brecOn.eq
-Tree.brecOn.go
-Tree.casesOn
-Tree.coe_treesOfNumNodesEq
-Tree.comp_map
-Tree.comp_traverse
-Tree.ctorElim
-Tree.ctorElimType
-Tree.ctorIdx
-Tree.height.eq_def
-Tree.height_le_numNodes
-Tree.id_map
-Tree.instInhabited
-Tree.instLawfulTraversable
-Tree.instTraversable
-Tree.left_node_right_eq_self
-Tree.map.eq_def
-Tree.mem_treesOfNumNodesEq
-Tree.mem_treesOfNumNodesEq_numNodes
-Tree.naturality
-Tree.nil.elim
-Tree.nil.sizeOf_spec
-Tree.noConfusion
-Tree.noConfusionType
-Tree.node.elim
-Tree.node.inj
-Tree.node.injEq
-Tree.node.noConfusion
-Tree.node.sizeOf_spec
-Tree.numLeaves.eq_def
-Tree.numLeaves_eq_numNodes_succ
-Tree.numLeaves_pos
-Tree.numNodes.eq_def
-Tree.pairwiseNode
-Tree.rec
-Tree.recOn
-Tree.traverse.eq_def
-Tree.traverse_eq_map_id
-Tree.traverse_pure
-Tree.treesOfNumNodesEq.eq_def
-Tree.treesOfNumNodesEq_card_eq_catalan
-Tree.treesOfNumNodesEq_succ
-Tree.treesOfNumNodesEq_zero
-Tree.«term_△_»
+instDecidableEqBinaryTree
+instDecidableEqBinaryTree.decEq
-instDecidableEqTree
-instDecidableEqTree.decEq
+instReprBinaryTree
+instReprBinaryTree.repr
-instReprTree
-instReprTree.repr

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 9ab2f22441
Reference commit d90090f647

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…ry_tree

sorrachai · 2026-06-08T09:29:27Z

Should I change anything?

eric-wieser · 2026-06-08T18:32:32Z

bors merge

Thanks!

mathlib-bors · 2026-06-08T18:32:36Z

👎 Rejected by label

eric-wieser · 2026-06-08T18:33:24Z

bors merge

Rename `Tree` to `BinaryTree`. This frees up the name `Tree` to cover n-ary trees in future. We only deprecate the `def`s, and move the theorems without deprecation. Co-authored-by: Eric Wieser <efw@google.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2026-06-08T19:11:57Z

Pull request successfully merged into master.

Build succeeded:

`Tree` was renamed to `BinaryTree` in leanprover-community#39707, but `docs/overview.yaml` still referred to the old name, failing the check-yaml post-build step. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…ty#39707) Rename `Tree` to `BinaryTree`. This frees up the name `Tree` to cover n-ary trees in future. We only deprecate the `def`s, and move the theorems without deprecation. Co-authored-by: Eric Wieser <efw@google.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

sorrachai added 8 commits May 22, 2026 14:27

rename tree; define memberaship instance; decidable; traversal

a629abf

author

9c3719f

update

952d13f

update

3df2975

minor

89256dd

change Tree to BinaryTree

7d8e49d

rename branch

a8a24c1

ensure only rename

8e7291a

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label May 22, 2026

minor

0fcd3b0

sorrachai mentioned this pull request May 22, 2026

feat(Data/Tree/Basic): add Membership instance, new notation, rename Tree #39697

Open

sorrachai requested a review from eric-wieser May 22, 2026 14:36

eric-wieser reviewed May 22, 2026

View reviewed changes

Comment thread Mathlib/Data/Tree/Basic.lean

eric-wieser reviewed May 22, 2026

View reviewed changes

Comment thread Mathlib/Data/Tree/Basic.lean

add deprecated tags

c14add8

eric-wieser reviewed May 22, 2026

View reviewed changes

Comment thread Mathlib/Data/Tree/Basic.lean Outdated

eric-wieser reviewed May 22, 2026

View reviewed changes

Comment thread Mathlib/Data/Tree/Basic.lean Outdated

sorrachai and others added 4 commits May 22, 2026 17:32

Update Mathlib/Data/Tree/Basic.lean

53b1d9b

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Update Mathlib/Data/Tree/Basic.lean

1e415ba

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Merge branch 'master' into rename_tree_to_binary_tree

8667728

update

d585249

eric-wieser reviewed May 22, 2026

View reviewed changes

Comment thread Mathlib/Data/Tree/Basic.lean

eric-wieser reviewed May 22, 2026

View reviewed changes

Comment thread Mathlib/Data/Tree/Basic.lean Outdated

eric-wieser reviewed May 22, 2026

View reviewed changes

Comment thread Mathlib/Data/Tree/Get.lean

sorrachai added 2 commits May 22, 2026 18:10

depreciate Get.lean

8cef643

minor

b01599b

eric-wieser reviewed May 22, 2026

View reviewed changes

Comment thread Mathlib/Data/Tree/Basic.lean Outdated

Comment thread Mathlib/Data/Tree/Basic.lean Outdated

Update Mathlib/Data/Tree/Basic.lean

c371e4f

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser reviewed Jun 8, 2026

View reviewed changes

Comment thread Mathlib/Data/Tree/Basic.lean Outdated

eric-wieser added 2 commits June 8, 2026 02:14

alias docstrings

bd8e8b0

missing deprecation

51c6e76

eric-wieser temporarily deployed to cache-upload-forks June 8, 2026 02:21 — with GitHub Actions Inactive

eric-wieser added 2 commits June 8, 2026 02:23

Merge remote-tracking branch 'origin/master' into rename_tree_to_bina…

cfb5cf3

…ry_tree

missing import

44ee70e

eric-wieser temporarily deployed to cache-upload-forks June 8, 2026 02:51 — with GitHub Actions Inactive

eric-wieser reviewed Jun 8, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean Outdated

Apply suggestion from @eric-wieser

16ffd59

eric-wieser temporarily deployed to cache-upload-forks June 8, 2026 14:45 — with GitHub Actions Inactive

eric-wieser added 2 commits June 8, 2026 08:36

Docstring and formatting

fdb4514

Fix bad line wrapping

2f1f2dd

eric-wieser temporarily deployed to cache-upload-forks June 8, 2026 16:16 — with GitHub Actions Inactive

Remove blank line

c564425

github-actions Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 8, 2026

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label Jun 8, 2026

Merge branch 'master' into rename_tree_to_binary_tree

9ab2f22

eric-wieser removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 8, 2026

eric-wieser temporarily deployed to cache-upload-forks June 8, 2026 19:10 — with GitHub Actions Inactive

mathlib-bors Bot changed the title ~~chore(Data/Tree/Basic): Rename Tree to BinaryTree~~ [Merged by Bors] - chore(Data/Tree/Basic): Rename Tree to BinaryTree Jun 8, 2026

mathlib-bors Bot closed this Jun 8, 2026

Uh oh!

Conversation

sorrachai commented May 22, 2026 • edited by eric-wieser Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 22, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented May 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 9ab2f22441

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sorrachai commented Jun 8, 2026

Uh oh!

Uh oh!

eric-wieser commented Jun 8, 2026

Uh oh!

mathlib-bors Bot commented Jun 8, 2026

Uh oh!

eric-wieser commented Jun 8, 2026

Uh oh!

mathlib-bors Bot commented Jun 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

sorrachai commented May 22, 2026 •

edited by eric-wieser

Loading

github-actions Bot commented May 22, 2026 •

edited

Loading